The Runtime Complexity (innermost) of the given CpxTRS could be proven to be BOUNDS(1, n^1).

0 CpxTRS
    ↳1 CpxTrsMatchBoundsTAProof (⇔, 110 ms)
    ↳2 BOUNDS(1, n^1)
    ↳3 CpxTrsToCdtProof (BOTH BOUNDS(ID, ID), 0 ms)
    ↳4 CdtProblem
        ↳5 CdtLeafRemovalProof (BOTH BOUNDS(ID, ID), 0 ms)
        ↳6 CdtProblem
        ↳7 CdtUsableRulesProof (⇔, 0 ms)
        ↳8 CdtProblem
        ↳9 CdtRuleRemovalProof (UPPER BOUND(ADD(n^2)), 186 ms)
        ↳10 CdtProblem
        ↳11 CdtNarrowingProof (BOTH BOUNDS(ID, ID), 0 ms)
        ↳12 CdtProblem
        ↳13 CdtRhsSimplificationProcessorProof (BOTH BOUNDS(ID, ID), 0 ms)
        ↳14 CdtProblem
        ↳15 CdtGraphSplitRhsProof (BOTH BOUNDS(ID, ID), 0 ms)
        ↳16 CdtProblem
        ↳17 CdtNarrowingProof (BOTH BOUNDS(ID, ID), 0 ms)
        ↳18 CdtProblem
        ↳19 CdtGraphSplitRhsProof (BOTH BOUNDS(ID, ID), 0 ms)
        ↳20 CdtProblem
        ↳21 CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID), 0 ms)
        ↳22 CdtProblem
        ↳23 CdtNarrowingProof (BOTH BOUNDS(ID, ID), 3 ms)
        ↳24 CdtProblem
        ↳25 CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID), 0 ms)
        ↳26 CdtProblem
        ↳27 CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID), 0 ms)
        ↳28 CdtProblem
        ↳29 CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID), 0 ms)
        ↳30 CdtProblem
        ↳31 CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID), 0 ms)
        ↳32 CdtProblem
        ↳33 CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID), 0 ms)
        ↳34 CdtProblem
        ↳35 CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID), 0 ms)
        ↳36 CdtProblem
        ↳37 CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID), 0 ms)
        ↳38 CdtProblem
        ↳39 CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID), 0 ms)
        ↳40 CdtProblem
        ↳41 CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID), 0 ms)
        ↳42 CdtProblem
        ↳43 CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID), 7 ms)
        ↳44 CdtProblem

(0) Obligation:

The Runtime Complexity (innermost) of the given CpxTRS could be proven to be BOUNDS(1, n^1).


The TRS R consists of the following rules:

max(L(x)) → x
max(N(L(0), L(y))) → y
max(N(L(s(x)), L(s(y)))) → s(max(N(L(x), L(y))))
max(N(L(x), N(y, z))) → max(N(L(x), L(max(N(y, z)))))

Rewrite Strategy: INNERMOST

(1) CpxTrsMatchBoundsTAProof (EQUIVALENT transformation)

A linear upper bound on the runtime complexity of the TRS R could be shown with a Match-Bound[TAB_LEFTLINEAR,TAB_NONLEFTLINEAR] (for contructor-based start-terms) of 1.

The compatible tree automaton used to show the Match-Boundedness (for constructor-based start-terms) is represented by:
final states : [1]
transitions:
L0(0) → 0
N0(0, 0) → 0
00() → 0
s0(0) → 0
max0(0) → 1
L1(0) → 4
L1(0) → 5
N1(4, 5) → 3
max1(3) → 2
s1(2) → 1
N1(0, 0) → 8
max1(8) → 7
L1(7) → 6
N1(4, 6) → 3
max1(3) → 1
s1(2) → 7
max1(3) → 7
L1(2) → 5
0 → 1
0 → 7
0 → 2
7 → 1
7 → 2
2 → 1
2 → 7

(2) BOUNDS(1, n^1)

(3) CpxTrsToCdtProof (BOTH BOUNDS(ID, ID) transformation)

Converted Cpx (relative) TRS to CDT

(4) Obligation:

Complexity Dependency Tuples Problem
Rules:

max(L(z0)) → z0
max(N(L(0), L(z0))) → z0
max(N(L(s(z0)), L(s(z1)))) → s(max(N(L(z0), L(z1))))
max(N(L(z0), N(z1, z2))) → max(N(L(z0), L(max(N(z1, z2)))))
Tuples:

MAX(L(z0)) → c
MAX(N(L(0), L(z0))) → c1
MAX(N(L(s(z0)), L(s(z1)))) → c2(MAX(N(L(z0), L(z1))))
MAX(N(L(z0), N(z1, z2))) → c3(MAX(N(L(z0), L(max(N(z1, z2))))), MAX(N(z1, z2)))
S tuples:

MAX(L(z0)) → c
MAX(N(L(0), L(z0))) → c1
MAX(N(L(s(z0)), L(s(z1)))) → c2(MAX(N(L(z0), L(z1))))
MAX(N(L(z0), N(z1, z2))) → c3(MAX(N(L(z0), L(max(N(z1, z2))))), MAX(N(z1, z2)))
K tuples:none
Defined Rule Symbols:

max

Defined Pair Symbols:

MAX

Compound Symbols:

c, c1, c2, c3

(5) CdtLeafRemovalProof (BOTH BOUNDS(ID, ID) transformation)

Removed 2 trailing nodes:

MAX(L(z0)) → c
MAX(N(L(0), L(z0))) → c1

(6) Obligation:

Complexity Dependency Tuples Problem
Rules:

max(L(z0)) → z0
max(N(L(0), L(z0))) → z0
max(N(L(s(z0)), L(s(z1)))) → s(max(N(L(z0), L(z1))))
max(N(L(z0), N(z1, z2))) → max(N(L(z0), L(max(N(z1, z2)))))
Tuples:

MAX(N(L(s(z0)), L(s(z1)))) → c2(MAX(N(L(z0), L(z1))))
MAX(N(L(z0), N(z1, z2))) → c3(MAX(N(L(z0), L(max(N(z1, z2))))), MAX(N(z1, z2)))
S tuples:

MAX(N(L(s(z0)), L(s(z1)))) → c2(MAX(N(L(z0), L(z1))))
MAX(N(L(z0), N(z1, z2))) → c3(MAX(N(L(z0), L(max(N(z1, z2))))), MAX(N(z1, z2)))
K tuples:none
Defined Rule Symbols:

max

Defined Pair Symbols:

MAX

Compound Symbols:

c2, c3

(7) CdtUsableRulesProof (EQUIVALENT transformation)

The following rules are not usable and were removed:

max(L(z0)) → z0

(8) Obligation:

Complexity Dependency Tuples Problem
Rules:

max(N(L(0), L(z0))) → z0
max(N(L(s(z0)), L(s(z1)))) → s(max(N(L(z0), L(z1))))
max(N(L(z0), N(z1, z2))) → max(N(L(z0), L(max(N(z1, z2)))))
Tuples:

MAX(N(L(s(z0)), L(s(z1)))) → c2(MAX(N(L(z0), L(z1))))
MAX(N(L(z0), N(z1, z2))) → c3(MAX(N(L(z0), L(max(N(z1, z2))))), MAX(N(z1, z2)))
S tuples:

MAX(N(L(s(z0)), L(s(z1)))) → c2(MAX(N(L(z0), L(z1))))
MAX(N(L(z0), N(z1, z2))) → c3(MAX(N(L(z0), L(max(N(z1, z2))))), MAX(N(z1, z2)))
K tuples:none
Defined Rule Symbols:

max

Defined Pair Symbols:

MAX

Compound Symbols:

c2, c3

(9) CdtRuleRemovalProof (UPPER BOUND(ADD(n^2)) transformation)

Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.

MAX(N(L(z0), N(z1, z2))) → c3(MAX(N(L(z0), L(max(N(z1, z2))))), MAX(N(z1, z2)))
We considered the (Usable) Rules:none
And the Tuples:

MAX(N(L(s(z0)), L(s(z1)))) → c2(MAX(N(L(z0), L(z1))))
MAX(N(L(z0), N(z1, z2))) → c3(MAX(N(L(z0), L(max(N(z1, z2))))), MAX(N(z1, z2)))
The order we found is given by the following interpretation:
Polynomial interpretation :

POL(0) = 0   
POL(L(x1)) = 0   
POL(MAX(x1)) = [1] + x12   
POL(N(x1, x2)) = [1] + x2   
POL(c2(x1)) = x1   
POL(c3(x1, x2)) = x1 + x2   
POL(max(x1)) = 0   
POL(s(x1)) = 0   

(10) Obligation:

Complexity Dependency Tuples Problem
Rules:

max(N(L(0), L(z0))) → z0
max(N(L(s(z0)), L(s(z1)))) → s(max(N(L(z0), L(z1))))
max(N(L(z0), N(z1, z2))) → max(N(L(z0), L(max(N(z1, z2)))))
Tuples:

MAX(N(L(s(z0)), L(s(z1)))) → c2(MAX(N(L(z0), L(z1))))
MAX(N(L(z0), N(z1, z2))) → c3(MAX(N(L(z0), L(max(N(z1, z2))))), MAX(N(z1, z2)))
S tuples:

MAX(N(L(s(z0)), L(s(z1)))) → c2(MAX(N(L(z0), L(z1))))
K tuples:

MAX(N(L(z0), N(z1, z2))) → c3(MAX(N(L(z0), L(max(N(z1, z2))))), MAX(N(z1, z2)))
Defined Rule Symbols:

max

Defined Pair Symbols:

MAX

Compound Symbols:

c2, c3

(11) CdtNarrowingProof (BOTH BOUNDS(ID, ID) transformation)

Use narrowing to replace MAX(N(L(z0), N(z1, z2))) → c3(MAX(N(L(z0), L(max(N(z1, z2))))), MAX(N(z1, z2))) by

MAX(N(L(x0), N(L(0), L(z0)))) → c3(MAX(N(L(x0), L(z0))), MAX(N(L(0), L(z0))))
MAX(N(L(x0), N(L(s(z0)), L(s(z1))))) → c3(MAX(N(L(x0), L(s(max(N(L(z0), L(z1))))))), MAX(N(L(s(z0)), L(s(z1)))))
MAX(N(L(x0), N(L(z0), N(z1, z2)))) → c3(MAX(N(L(x0), L(max(N(L(z0), L(max(N(z1, z2)))))))), MAX(N(L(z0), N(z1, z2))))

(12) Obligation:

Complexity Dependency Tuples Problem
Rules:

max(N(L(0), L(z0))) → z0
max(N(L(s(z0)), L(s(z1)))) → s(max(N(L(z0), L(z1))))
max(N(L(z0), N(z1, z2))) → max(N(L(z0), L(max(N(z1, z2)))))
Tuples:

MAX(N(L(s(z0)), L(s(z1)))) → c2(MAX(N(L(z0), L(z1))))
MAX(N(L(x0), N(L(0), L(z0)))) → c3(MAX(N(L(x0), L(z0))), MAX(N(L(0), L(z0))))
MAX(N(L(x0), N(L(s(z0)), L(s(z1))))) → c3(MAX(N(L(x0), L(s(max(N(L(z0), L(z1))))))), MAX(N(L(s(z0)), L(s(z1)))))
MAX(N(L(x0), N(L(z0), N(z1, z2)))) → c3(MAX(N(L(x0), L(max(N(L(z0), L(max(N(z1, z2)))))))), MAX(N(L(z0), N(z1, z2))))
S tuples:

MAX(N(L(s(z0)), L(s(z1)))) → c2(MAX(N(L(z0), L(z1))))
K tuples:

MAX(N(L(z0), N(z1, z2))) → c3(MAX(N(L(z0), L(max(N(z1, z2))))), MAX(N(z1, z2)))
Defined Rule Symbols:

max

Defined Pair Symbols:

MAX

Compound Symbols:

c2, c3

(13) CdtRhsSimplificationProcessorProof (BOTH BOUNDS(ID, ID) transformation)

Removed 1 trailing tuple parts

(14) Obligation:

Complexity Dependency Tuples Problem
Rules:

max(N(L(0), L(z0))) → z0
max(N(L(s(z0)), L(s(z1)))) → s(max(N(L(z0), L(z1))))
max(N(L(z0), N(z1, z2))) → max(N(L(z0), L(max(N(z1, z2)))))
Tuples:

MAX(N(L(s(z0)), L(s(z1)))) → c2(MAX(N(L(z0), L(z1))))
MAX(N(L(x0), N(L(s(z0)), L(s(z1))))) → c3(MAX(N(L(x0), L(s(max(N(L(z0), L(z1))))))), MAX(N(L(s(z0)), L(s(z1)))))
MAX(N(L(x0), N(L(z0), N(z1, z2)))) → c3(MAX(N(L(x0), L(max(N(L(z0), L(max(N(z1, z2)))))))), MAX(N(L(z0), N(z1, z2))))
MAX(N(L(x0), N(L(0), L(z0)))) → c3(MAX(N(L(x0), L(z0))))
S tuples:

MAX(N(L(s(z0)), L(s(z1)))) → c2(MAX(N(L(z0), L(z1))))
K tuples:

MAX(N(L(z0), N(z1, z2))) → c3(MAX(N(L(z0), L(max(N(z1, z2))))), MAX(N(z1, z2)))
Defined Rule Symbols:

max

Defined Pair Symbols:

MAX

Compound Symbols:

c2, c3, c3

(15) CdtGraphSplitRhsProof (BOTH BOUNDS(ID, ID) transformation)

Split RHS of tuples not part of any SCC

(16) Obligation:

Complexity Dependency Tuples Problem
Rules:

max(N(L(0), L(z0))) → z0
max(N(L(s(z0)), L(s(z1)))) → s(max(N(L(z0), L(z1))))
max(N(L(z0), N(z1, z2))) → max(N(L(z0), L(max(N(z1, z2)))))
Tuples:

MAX(N(L(s(z0)), L(s(z1)))) → c2(MAX(N(L(z0), L(z1))))
MAX(N(L(x0), N(L(z0), N(z1, z2)))) → c3(MAX(N(L(x0), L(max(N(L(z0), L(max(N(z1, z2)))))))), MAX(N(L(z0), N(z1, z2))))
MAX(N(L(x0), N(L(0), L(z0)))) → c3(MAX(N(L(x0), L(z0))))
MAX(N(L(x0), N(L(s(z0)), L(s(z1))))) → c(MAX(N(L(x0), L(s(max(N(L(z0), L(z1))))))))
MAX(N(L(x0), N(L(s(z0)), L(s(z1))))) → c(MAX(N(L(s(z0)), L(s(z1)))))
S tuples:

MAX(N(L(s(z0)), L(s(z1)))) → c2(MAX(N(L(z0), L(z1))))
K tuples:

MAX(N(L(z0), N(z1, z2))) → c3(MAX(N(L(z0), L(max(N(z1, z2))))), MAX(N(z1, z2)))
Defined Rule Symbols:

max

Defined Pair Symbols:

MAX

Compound Symbols:

c2, c3, c3, c

(17) CdtNarrowingProof (BOTH BOUNDS(ID, ID) transformation)

Use narrowing to replace MAX(N(L(x0), N(L(z0), N(z1, z2)))) → c3(MAX(N(L(x0), L(max(N(L(z0), L(max(N(z1, z2)))))))), MAX(N(L(z0), N(z1, z2)))) by

MAX(N(L(x0), N(L(0), N(x2, x3)))) → c3(MAX(N(L(x0), L(max(N(x2, x3))))), MAX(N(L(0), N(x2, x3))))
MAX(N(L(x0), N(L(x1), N(L(0), L(z0))))) → c3(MAX(N(L(x0), L(max(N(L(x1), L(z0)))))), MAX(N(L(x1), N(L(0), L(z0)))))
MAX(N(L(x0), N(L(x1), N(L(s(z0)), L(s(z1)))))) → c3(MAX(N(L(x0), L(max(N(L(x1), L(s(max(N(L(z0), L(z1)))))))))), MAX(N(L(x1), N(L(s(z0)), L(s(z1))))))
MAX(N(L(x0), N(L(x1), N(L(z0), N(z1, z2))))) → c3(MAX(N(L(x0), L(max(N(L(x1), L(max(N(L(z0), L(max(N(z1, z2))))))))))), MAX(N(L(x1), N(L(z0), N(z1, z2)))))

(18) Obligation:

Complexity Dependency Tuples Problem
Rules:

max(N(L(0), L(z0))) → z0
max(N(L(s(z0)), L(s(z1)))) → s(max(N(L(z0), L(z1))))
max(N(L(z0), N(z1, z2))) → max(N(L(z0), L(max(N(z1, z2)))))
Tuples:

MAX(N(L(s(z0)), L(s(z1)))) → c2(MAX(N(L(z0), L(z1))))
MAX(N(L(x0), N(L(0), L(z0)))) → c3(MAX(N(L(x0), L(z0))))
MAX(N(L(x0), N(L(s(z0)), L(s(z1))))) → c(MAX(N(L(x0), L(s(max(N(L(z0), L(z1))))))))
MAX(N(L(x0), N(L(s(z0)), L(s(z1))))) → c(MAX(N(L(s(z0)), L(s(z1)))))
MAX(N(L(x0), N(L(0), N(x2, x3)))) → c3(MAX(N(L(x0), L(max(N(x2, x3))))), MAX(N(L(0), N(x2, x3))))
MAX(N(L(x0), N(L(x1), N(L(0), L(z0))))) → c3(MAX(N(L(x0), L(max(N(L(x1), L(z0)))))), MAX(N(L(x1), N(L(0), L(z0)))))
MAX(N(L(x0), N(L(x1), N(L(s(z0)), L(s(z1)))))) → c3(MAX(N(L(x0), L(max(N(L(x1), L(s(max(N(L(z0), L(z1)))))))))), MAX(N(L(x1), N(L(s(z0)), L(s(z1))))))
MAX(N(L(x0), N(L(x1), N(L(z0), N(z1, z2))))) → c3(MAX(N(L(x0), L(max(N(L(x1), L(max(N(L(z0), L(max(N(z1, z2))))))))))), MAX(N(L(x1), N(L(z0), N(z1, z2)))))
S tuples:

MAX(N(L(s(z0)), L(s(z1)))) → c2(MAX(N(L(z0), L(z1))))
K tuples:

MAX(N(L(z0), N(z1, z2))) → c3(MAX(N(L(z0), L(max(N(z1, z2))))), MAX(N(z1, z2)))
Defined Rule Symbols:

max

Defined Pair Symbols:

MAX

Compound Symbols:

c2, c3, c, c3

(19) CdtGraphSplitRhsProof (BOTH BOUNDS(ID, ID) transformation)

Split RHS of tuples not part of any SCC

(20) Obligation:

Complexity Dependency Tuples Problem
Rules:

max(N(L(0), L(z0))) → z0
max(N(L(s(z0)), L(s(z1)))) → s(max(N(L(z0), L(z1))))
max(N(L(z0), N(z1, z2))) → max(N(L(z0), L(max(N(z1, z2)))))
Tuples:

MAX(N(L(s(z0)), L(s(z1)))) → c2(MAX(N(L(z0), L(z1))))
MAX(N(L(x0), N(L(0), L(z0)))) → c3(MAX(N(L(x0), L(z0))))
MAX(N(L(x0), N(L(s(z0)), L(s(z1))))) → c(MAX(N(L(x0), L(s(max(N(L(z0), L(z1))))))))
MAX(N(L(x0), N(L(s(z0)), L(s(z1))))) → c(MAX(N(L(s(z0)), L(s(z1)))))
MAX(N(L(x0), N(L(0), N(x2, x3)))) → c3(MAX(N(L(x0), L(max(N(x2, x3))))), MAX(N(L(0), N(x2, x3))))
MAX(N(L(x0), N(L(x1), N(L(z0), N(z1, z2))))) → c3(MAX(N(L(x0), L(max(N(L(x1), L(max(N(L(z0), L(max(N(z1, z2))))))))))), MAX(N(L(x1), N(L(z0), N(z1, z2)))))
MAX(N(L(x0), N(L(x1), N(L(0), L(z0))))) → c1(MAX(N(L(x0), L(max(N(L(x1), L(z0)))))))
MAX(N(L(x0), N(L(x1), N(L(0), L(z0))))) → c1(MAX(N(L(x1), N(L(0), L(z0)))))
MAX(N(L(x0), N(L(x1), N(L(s(z0)), L(s(z1)))))) → c1(MAX(N(L(x0), L(max(N(L(x1), L(s(max(N(L(z0), L(z1)))))))))))
MAX(N(L(x0), N(L(x1), N(L(s(z0)), L(s(z1)))))) → c1(MAX(N(L(x1), N(L(s(z0)), L(s(z1))))))
S tuples:

MAX(N(L(s(z0)), L(s(z1)))) → c2(MAX(N(L(z0), L(z1))))
K tuples:

MAX(N(L(z0), N(z1, z2))) → c3(MAX(N(L(z0), L(max(N(z1, z2))))), MAX(N(z1, z2)))
Defined Rule Symbols:

max

Defined Pair Symbols:

MAX

Compound Symbols:

c2, c3, c, c3, c1

(21) CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID) transformation)

Use forward instantiation to replace MAX(N(L(s(z0)), L(s(z1)))) → c2(MAX(N(L(z0), L(z1)))) by

MAX(N(L(s(s(y0))), L(s(s(y1))))) → c2(MAX(N(L(s(y0)), L(s(y1)))))

(22) Obligation:

Complexity Dependency Tuples Problem
Rules:

max(N(L(0), L(z0))) → z0
max(N(L(s(z0)), L(s(z1)))) → s(max(N(L(z0), L(z1))))
max(N(L(z0), N(z1, z2))) → max(N(L(z0), L(max(N(z1, z2)))))
Tuples:

MAX(N(L(x0), N(L(0), L(z0)))) → c3(MAX(N(L(x0), L(z0))))
MAX(N(L(x0), N(L(s(z0)), L(s(z1))))) → c(MAX(N(L(x0), L(s(max(N(L(z0), L(z1))))))))
MAX(N(L(x0), N(L(s(z0)), L(s(z1))))) → c(MAX(N(L(s(z0)), L(s(z1)))))
MAX(N(L(x0), N(L(0), N(x2, x3)))) → c3(MAX(N(L(x0), L(max(N(x2, x3))))), MAX(N(L(0), N(x2, x3))))
MAX(N(L(x0), N(L(x1), N(L(z0), N(z1, z2))))) → c3(MAX(N(L(x0), L(max(N(L(x1), L(max(N(L(z0), L(max(N(z1, z2))))))))))), MAX(N(L(x1), N(L(z0), N(z1, z2)))))
MAX(N(L(x0), N(L(x1), N(L(0), L(z0))))) → c1(MAX(N(L(x0), L(max(N(L(x1), L(z0)))))))
MAX(N(L(x0), N(L(x1), N(L(0), L(z0))))) → c1(MAX(N(L(x1), N(L(0), L(z0)))))
MAX(N(L(x0), N(L(x1), N(L(s(z0)), L(s(z1)))))) → c1(MAX(N(L(x0), L(max(N(L(x1), L(s(max(N(L(z0), L(z1)))))))))))
MAX(N(L(x0), N(L(x1), N(L(s(z0)), L(s(z1)))))) → c1(MAX(N(L(x1), N(L(s(z0)), L(s(z1))))))
MAX(N(L(s(s(y0))), L(s(s(y1))))) → c2(MAX(N(L(s(y0)), L(s(y1)))))
S tuples:

MAX(N(L(s(s(y0))), L(s(s(y1))))) → c2(MAX(N(L(s(y0)), L(s(y1)))))
K tuples:

MAX(N(L(z0), N(z1, z2))) → c3(MAX(N(L(z0), L(max(N(z1, z2))))), MAX(N(z1, z2)))
Defined Rule Symbols:

max

Defined Pair Symbols:

MAX

Compound Symbols:

c3, c, c3, c1, c2

(23) CdtNarrowingProof (BOTH BOUNDS(ID, ID) transformation)

Use narrowing to replace MAX(N(L(x0), N(L(s(z0)), L(s(z1))))) → c(MAX(N(L(x0), L(s(max(N(L(z0), L(z1)))))))) by

MAX(N(L(x0), N(L(s(0)), L(s(z0))))) → c(MAX(N(L(x0), L(s(z0)))))
MAX(N(L(x0), N(L(s(s(z0))), L(s(s(z1)))))) → c(MAX(N(L(x0), L(s(s(max(N(L(z0), L(z1)))))))))

(24) Obligation:

Complexity Dependency Tuples Problem
Rules:

max(N(L(0), L(z0))) → z0
max(N(L(s(z0)), L(s(z1)))) → s(max(N(L(z0), L(z1))))
max(N(L(z0), N(z1, z2))) → max(N(L(z0), L(max(N(z1, z2)))))
Tuples:

MAX(N(L(x0), N(L(0), L(z0)))) → c3(MAX(N(L(x0), L(z0))))
MAX(N(L(x0), N(L(s(z0)), L(s(z1))))) → c(MAX(N(L(s(z0)), L(s(z1)))))
MAX(N(L(x0), N(L(0), N(x2, x3)))) → c3(MAX(N(L(x0), L(max(N(x2, x3))))), MAX(N(L(0), N(x2, x3))))
MAX(N(L(x0), N(L(x1), N(L(z0), N(z1, z2))))) → c3(MAX(N(L(x0), L(max(N(L(x1), L(max(N(L(z0), L(max(N(z1, z2))))))))))), MAX(N(L(x1), N(L(z0), N(z1, z2)))))
MAX(N(L(x0), N(L(x1), N(L(0), L(z0))))) → c1(MAX(N(L(x0), L(max(N(L(x1), L(z0)))))))
MAX(N(L(x0), N(L(x1), N(L(0), L(z0))))) → c1(MAX(N(L(x1), N(L(0), L(z0)))))
MAX(N(L(x0), N(L(x1), N(L(s(z0)), L(s(z1)))))) → c1(MAX(N(L(x0), L(max(N(L(x1), L(s(max(N(L(z0), L(z1)))))))))))
MAX(N(L(x0), N(L(x1), N(L(s(z0)), L(s(z1)))))) → c1(MAX(N(L(x1), N(L(s(z0)), L(s(z1))))))
MAX(N(L(s(s(y0))), L(s(s(y1))))) → c2(MAX(N(L(s(y0)), L(s(y1)))))
MAX(N(L(x0), N(L(s(0)), L(s(z0))))) → c(MAX(N(L(x0), L(s(z0)))))
MAX(N(L(x0), N(L(s(s(z0))), L(s(s(z1)))))) → c(MAX(N(L(x0), L(s(s(max(N(L(z0), L(z1)))))))))
S tuples:

MAX(N(L(s(s(y0))), L(s(s(y1))))) → c2(MAX(N(L(s(y0)), L(s(y1)))))
K tuples:

MAX(N(L(z0), N(z1, z2))) → c3(MAX(N(L(z0), L(max(N(z1, z2))))), MAX(N(z1, z2)))
Defined Rule Symbols:

max

Defined Pair Symbols:

MAX

Compound Symbols:

c3, c, c3, c1, c2

(25) CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID) transformation)

Use forward instantiation to replace MAX(N(L(x0), N(L(0), L(z0)))) → c3(MAX(N(L(x0), L(z0)))) by

MAX(N(L(s(s(y0))), N(L(0), L(s(s(y1)))))) → c3(MAX(N(L(s(s(y0))), L(s(s(y1))))))

(26) Obligation:

Complexity Dependency Tuples Problem
Rules:

max(N(L(0), L(z0))) → z0
max(N(L(s(z0)), L(s(z1)))) → s(max(N(L(z0), L(z1))))
max(N(L(z0), N(z1, z2))) → max(N(L(z0), L(max(N(z1, z2)))))
Tuples:

MAX(N(L(x0), N(L(s(z0)), L(s(z1))))) → c(MAX(N(L(s(z0)), L(s(z1)))))
MAX(N(L(x0), N(L(0), N(x2, x3)))) → c3(MAX(N(L(x0), L(max(N(x2, x3))))), MAX(N(L(0), N(x2, x3))))
MAX(N(L(x0), N(L(x1), N(L(z0), N(z1, z2))))) → c3(MAX(N(L(x0), L(max(N(L(x1), L(max(N(L(z0), L(max(N(z1, z2))))))))))), MAX(N(L(x1), N(L(z0), N(z1, z2)))))
MAX(N(L(x0), N(L(x1), N(L(0), L(z0))))) → c1(MAX(N(L(x0), L(max(N(L(x1), L(z0)))))))
MAX(N(L(x0), N(L(x1), N(L(0), L(z0))))) → c1(MAX(N(L(x1), N(L(0), L(z0)))))
MAX(N(L(x0), N(L(x1), N(L(s(z0)), L(s(z1)))))) → c1(MAX(N(L(x0), L(max(N(L(x1), L(s(max(N(L(z0), L(z1)))))))))))
MAX(N(L(x0), N(L(x1), N(L(s(z0)), L(s(z1)))))) → c1(MAX(N(L(x1), N(L(s(z0)), L(s(z1))))))
MAX(N(L(s(s(y0))), L(s(s(y1))))) → c2(MAX(N(L(s(y0)), L(s(y1)))))
MAX(N(L(x0), N(L(s(0)), L(s(z0))))) → c(MAX(N(L(x0), L(s(z0)))))
MAX(N(L(x0), N(L(s(s(z0))), L(s(s(z1)))))) → c(MAX(N(L(x0), L(s(s(max(N(L(z0), L(z1)))))))))
MAX(N(L(s(s(y0))), N(L(0), L(s(s(y1)))))) → c3(MAX(N(L(s(s(y0))), L(s(s(y1))))))
S tuples:

MAX(N(L(s(s(y0))), L(s(s(y1))))) → c2(MAX(N(L(s(y0)), L(s(y1)))))
K tuples:

MAX(N(L(z0), N(z1, z2))) → c3(MAX(N(L(z0), L(max(N(z1, z2))))), MAX(N(z1, z2)))
Defined Rule Symbols:

max

Defined Pair Symbols:

MAX

Compound Symbols:

c, c3, c1, c2, c3

(27) CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID) transformation)

Use forward instantiation to replace MAX(N(L(x0), N(L(s(z0)), L(s(z1))))) → c(MAX(N(L(s(z0)), L(s(z1))))) by

MAX(N(L(z0), N(L(s(s(y0))), L(s(s(y1)))))) → c(MAX(N(L(s(s(y0))), L(s(s(y1))))))

(28) Obligation:

Complexity Dependency Tuples Problem
Rules:

max(N(L(0), L(z0))) → z0
max(N(L(s(z0)), L(s(z1)))) → s(max(N(L(z0), L(z1))))
max(N(L(z0), N(z1, z2))) → max(N(L(z0), L(max(N(z1, z2)))))
Tuples:

MAX(N(L(x0), N(L(0), N(x2, x3)))) → c3(MAX(N(L(x0), L(max(N(x2, x3))))), MAX(N(L(0), N(x2, x3))))
MAX(N(L(x0), N(L(x1), N(L(z0), N(z1, z2))))) → c3(MAX(N(L(x0), L(max(N(L(x1), L(max(N(L(z0), L(max(N(z1, z2))))))))))), MAX(N(L(x1), N(L(z0), N(z1, z2)))))
MAX(N(L(x0), N(L(x1), N(L(0), L(z0))))) → c1(MAX(N(L(x0), L(max(N(L(x1), L(z0)))))))
MAX(N(L(x0), N(L(x1), N(L(0), L(z0))))) → c1(MAX(N(L(x1), N(L(0), L(z0)))))
MAX(N(L(x0), N(L(x1), N(L(s(z0)), L(s(z1)))))) → c1(MAX(N(L(x0), L(max(N(L(x1), L(s(max(N(L(z0), L(z1)))))))))))
MAX(N(L(x0), N(L(x1), N(L(s(z0)), L(s(z1)))))) → c1(MAX(N(L(x1), N(L(s(z0)), L(s(z1))))))
MAX(N(L(s(s(y0))), L(s(s(y1))))) → c2(MAX(N(L(s(y0)), L(s(y1)))))
MAX(N(L(x0), N(L(s(0)), L(s(z0))))) → c(MAX(N(L(x0), L(s(z0)))))
MAX(N(L(x0), N(L(s(s(z0))), L(s(s(z1)))))) → c(MAX(N(L(x0), L(s(s(max(N(L(z0), L(z1)))))))))
MAX(N(L(s(s(y0))), N(L(0), L(s(s(y1)))))) → c3(MAX(N(L(s(s(y0))), L(s(s(y1))))))
MAX(N(L(z0), N(L(s(s(y0))), L(s(s(y1)))))) → c(MAX(N(L(s(s(y0))), L(s(s(y1))))))
S tuples:

MAX(N(L(s(s(y0))), L(s(s(y1))))) → c2(MAX(N(L(s(y0)), L(s(y1)))))
K tuples:

MAX(N(L(z0), N(z1, z2))) → c3(MAX(N(L(z0), L(max(N(z1, z2))))), MAX(N(z1, z2)))
Defined Rule Symbols:

max

Defined Pair Symbols:

MAX

Compound Symbols:

c3, c1, c2, c, c3

(29) CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID) transformation)

Use forward instantiation to replace MAX(N(L(x0), N(L(x1), N(L(0), L(z0))))) → c1(MAX(N(L(x1), N(L(0), L(z0))))) by

MAX(N(L(z0), N(L(s(s(y0))), N(L(0), L(s(s(y1))))))) → c1(MAX(N(L(s(s(y0))), N(L(0), L(s(s(y1)))))))

(30) Obligation:

Complexity Dependency Tuples Problem
Rules:

max(N(L(0), L(z0))) → z0
max(N(L(s(z0)), L(s(z1)))) → s(max(N(L(z0), L(z1))))
max(N(L(z0), N(z1, z2))) → max(N(L(z0), L(max(N(z1, z2)))))
Tuples:

MAX(N(L(x0), N(L(0), N(x2, x3)))) → c3(MAX(N(L(x0), L(max(N(x2, x3))))), MAX(N(L(0), N(x2, x3))))
MAX(N(L(x0), N(L(x1), N(L(z0), N(z1, z2))))) → c3(MAX(N(L(x0), L(max(N(L(x1), L(max(N(L(z0), L(max(N(z1, z2))))))))))), MAX(N(L(x1), N(L(z0), N(z1, z2)))))
MAX(N(L(x0), N(L(x1), N(L(0), L(z0))))) → c1(MAX(N(L(x0), L(max(N(L(x1), L(z0)))))))
MAX(N(L(x0), N(L(x1), N(L(s(z0)), L(s(z1)))))) → c1(MAX(N(L(x0), L(max(N(L(x1), L(s(max(N(L(z0), L(z1)))))))))))
MAX(N(L(x0), N(L(x1), N(L(s(z0)), L(s(z1)))))) → c1(MAX(N(L(x1), N(L(s(z0)), L(s(z1))))))
MAX(N(L(s(s(y0))), L(s(s(y1))))) → c2(MAX(N(L(s(y0)), L(s(y1)))))
MAX(N(L(x0), N(L(s(0)), L(s(z0))))) → c(MAX(N(L(x0), L(s(z0)))))
MAX(N(L(x0), N(L(s(s(z0))), L(s(s(z1)))))) → c(MAX(N(L(x0), L(s(s(max(N(L(z0), L(z1)))))))))
MAX(N(L(s(s(y0))), N(L(0), L(s(s(y1)))))) → c3(MAX(N(L(s(s(y0))), L(s(s(y1))))))
MAX(N(L(z0), N(L(s(s(y0))), L(s(s(y1)))))) → c(MAX(N(L(s(s(y0))), L(s(s(y1))))))
MAX(N(L(z0), N(L(s(s(y0))), N(L(0), L(s(s(y1))))))) → c1(MAX(N(L(s(s(y0))), N(L(0), L(s(s(y1)))))))
S tuples:

MAX(N(L(s(s(y0))), L(s(s(y1))))) → c2(MAX(N(L(s(y0)), L(s(y1)))))
K tuples:

MAX(N(L(z0), N(z1, z2))) → c3(MAX(N(L(z0), L(max(N(z1, z2))))), MAX(N(z1, z2)))
Defined Rule Symbols:

max

Defined Pair Symbols:

MAX

Compound Symbols:

c3, c1, c2, c, c3

(31) CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID) transformation)

Use forward instantiation to replace MAX(N(L(x0), N(L(x1), N(L(s(z0)), L(s(z1)))))) → c1(MAX(N(L(x1), N(L(s(z0)), L(s(z1)))))) by

MAX(N(L(z0), N(L(z1), N(L(s(0)), L(s(z3)))))) → c1(MAX(N(L(z1), N(L(s(0)), L(s(z3))))))
MAX(N(L(z0), N(L(z1), N(L(s(s(y1))), L(s(s(y2))))))) → c1(MAX(N(L(z1), N(L(s(s(y1))), L(s(s(y2)))))))

(32) Obligation:

Complexity Dependency Tuples Problem
Rules:

max(N(L(0), L(z0))) → z0
max(N(L(s(z0)), L(s(z1)))) → s(max(N(L(z0), L(z1))))
max(N(L(z0), N(z1, z2))) → max(N(L(z0), L(max(N(z1, z2)))))
Tuples:

MAX(N(L(x0), N(L(0), N(x2, x3)))) → c3(MAX(N(L(x0), L(max(N(x2, x3))))), MAX(N(L(0), N(x2, x3))))
MAX(N(L(x0), N(L(x1), N(L(z0), N(z1, z2))))) → c3(MAX(N(L(x0), L(max(N(L(x1), L(max(N(L(z0), L(max(N(z1, z2))))))))))), MAX(N(L(x1), N(L(z0), N(z1, z2)))))
MAX(N(L(x0), N(L(x1), N(L(0), L(z0))))) → c1(MAX(N(L(x0), L(max(N(L(x1), L(z0)))))))
MAX(N(L(x0), N(L(x1), N(L(s(z0)), L(s(z1)))))) → c1(MAX(N(L(x0), L(max(N(L(x1), L(s(max(N(L(z0), L(z1)))))))))))
MAX(N(L(s(s(y0))), L(s(s(y1))))) → c2(MAX(N(L(s(y0)), L(s(y1)))))
MAX(N(L(x0), N(L(s(0)), L(s(z0))))) → c(MAX(N(L(x0), L(s(z0)))))
MAX(N(L(x0), N(L(s(s(z0))), L(s(s(z1)))))) → c(MAX(N(L(x0), L(s(s(max(N(L(z0), L(z1)))))))))
MAX(N(L(s(s(y0))), N(L(0), L(s(s(y1)))))) → c3(MAX(N(L(s(s(y0))), L(s(s(y1))))))
MAX(N(L(z0), N(L(s(s(y0))), L(s(s(y1)))))) → c(MAX(N(L(s(s(y0))), L(s(s(y1))))))
MAX(N(L(z0), N(L(s(s(y0))), N(L(0), L(s(s(y1))))))) → c1(MAX(N(L(s(s(y0))), N(L(0), L(s(s(y1)))))))
MAX(N(L(z0), N(L(z1), N(L(s(0)), L(s(z3)))))) → c1(MAX(N(L(z1), N(L(s(0)), L(s(z3))))))
MAX(N(L(z0), N(L(z1), N(L(s(s(y1))), L(s(s(y2))))))) → c1(MAX(N(L(z1), N(L(s(s(y1))), L(s(s(y2)))))))
S tuples:

MAX(N(L(s(s(y0))), L(s(s(y1))))) → c2(MAX(N(L(s(y0)), L(s(y1)))))
K tuples:

MAX(N(L(z0), N(z1, z2))) → c3(MAX(N(L(z0), L(max(N(z1, z2))))), MAX(N(z1, z2)))
Defined Rule Symbols:

max

Defined Pair Symbols:

MAX

Compound Symbols:

c3, c1, c2, c, c3

(33) CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID) transformation)

Use forward instantiation to replace MAX(N(L(s(s(y0))), L(s(s(y1))))) → c2(MAX(N(L(s(y0)), L(s(y1))))) by

MAX(N(L(s(s(s(y0)))), L(s(s(s(y1)))))) → c2(MAX(N(L(s(s(y0))), L(s(s(y1))))))

(34) Obligation:

Complexity Dependency Tuples Problem
Rules:

max(N(L(0), L(z0))) → z0
max(N(L(s(z0)), L(s(z1)))) → s(max(N(L(z0), L(z1))))
max(N(L(z0), N(z1, z2))) → max(N(L(z0), L(max(N(z1, z2)))))
Tuples:

MAX(N(L(x0), N(L(0), N(x2, x3)))) → c3(MAX(N(L(x0), L(max(N(x2, x3))))), MAX(N(L(0), N(x2, x3))))
MAX(N(L(x0), N(L(x1), N(L(z0), N(z1, z2))))) → c3(MAX(N(L(x0), L(max(N(L(x1), L(max(N(L(z0), L(max(N(z1, z2))))))))))), MAX(N(L(x1), N(L(z0), N(z1, z2)))))
MAX(N(L(x0), N(L(x1), N(L(0), L(z0))))) → c1(MAX(N(L(x0), L(max(N(L(x1), L(z0)))))))
MAX(N(L(x0), N(L(x1), N(L(s(z0)), L(s(z1)))))) → c1(MAX(N(L(x0), L(max(N(L(x1), L(s(max(N(L(z0), L(z1)))))))))))
MAX(N(L(x0), N(L(s(0)), L(s(z0))))) → c(MAX(N(L(x0), L(s(z0)))))
MAX(N(L(x0), N(L(s(s(z0))), L(s(s(z1)))))) → c(MAX(N(L(x0), L(s(s(max(N(L(z0), L(z1)))))))))
MAX(N(L(s(s(y0))), N(L(0), L(s(s(y1)))))) → c3(MAX(N(L(s(s(y0))), L(s(s(y1))))))
MAX(N(L(z0), N(L(s(s(y0))), L(s(s(y1)))))) → c(MAX(N(L(s(s(y0))), L(s(s(y1))))))
MAX(N(L(z0), N(L(s(s(y0))), N(L(0), L(s(s(y1))))))) → c1(MAX(N(L(s(s(y0))), N(L(0), L(s(s(y1)))))))
MAX(N(L(z0), N(L(z1), N(L(s(0)), L(s(z3)))))) → c1(MAX(N(L(z1), N(L(s(0)), L(s(z3))))))
MAX(N(L(z0), N(L(z1), N(L(s(s(y1))), L(s(s(y2))))))) → c1(MAX(N(L(z1), N(L(s(s(y1))), L(s(s(y2)))))))
MAX(N(L(s(s(s(y0)))), L(s(s(s(y1)))))) → c2(MAX(N(L(s(s(y0))), L(s(s(y1))))))
S tuples:

MAX(N(L(s(s(s(y0)))), L(s(s(s(y1)))))) → c2(MAX(N(L(s(s(y0))), L(s(s(y1))))))
K tuples:

MAX(N(L(z0), N(z1, z2))) → c3(MAX(N(L(z0), L(max(N(z1, z2))))), MAX(N(z1, z2)))
Defined Rule Symbols:

max

Defined Pair Symbols:

MAX

Compound Symbols:

c3, c1, c, c3, c2

(35) CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID) transformation)

Use forward instantiation to replace MAX(N(L(x0), N(L(s(0)), L(s(z0))))) → c(MAX(N(L(x0), L(s(z0))))) by

MAX(N(L(s(s(s(y0)))), N(L(s(0)), L(s(s(s(y1))))))) → c(MAX(N(L(s(s(s(y0)))), L(s(s(s(y1)))))))

(36) Obligation:

Complexity Dependency Tuples Problem
Rules:

max(N(L(0), L(z0))) → z0
max(N(L(s(z0)), L(s(z1)))) → s(max(N(L(z0), L(z1))))
max(N(L(z0), N(z1, z2))) → max(N(L(z0), L(max(N(z1, z2)))))
Tuples:

MAX(N(L(x0), N(L(0), N(x2, x3)))) → c3(MAX(N(L(x0), L(max(N(x2, x3))))), MAX(N(L(0), N(x2, x3))))
MAX(N(L(x0), N(L(x1), N(L(z0), N(z1, z2))))) → c3(MAX(N(L(x0), L(max(N(L(x1), L(max(N(L(z0), L(max(N(z1, z2))))))))))), MAX(N(L(x1), N(L(z0), N(z1, z2)))))
MAX(N(L(x0), N(L(x1), N(L(0), L(z0))))) → c1(MAX(N(L(x0), L(max(N(L(x1), L(z0)))))))
MAX(N(L(x0), N(L(x1), N(L(s(z0)), L(s(z1)))))) → c1(MAX(N(L(x0), L(max(N(L(x1), L(s(max(N(L(z0), L(z1)))))))))))
MAX(N(L(x0), N(L(s(s(z0))), L(s(s(z1)))))) → c(MAX(N(L(x0), L(s(s(max(N(L(z0), L(z1)))))))))
MAX(N(L(s(s(y0))), N(L(0), L(s(s(y1)))))) → c3(MAX(N(L(s(s(y0))), L(s(s(y1))))))
MAX(N(L(z0), N(L(s(s(y0))), L(s(s(y1)))))) → c(MAX(N(L(s(s(y0))), L(s(s(y1))))))
MAX(N(L(z0), N(L(s(s(y0))), N(L(0), L(s(s(y1))))))) → c1(MAX(N(L(s(s(y0))), N(L(0), L(s(s(y1)))))))
MAX(N(L(z0), N(L(z1), N(L(s(0)), L(s(z3)))))) → c1(MAX(N(L(z1), N(L(s(0)), L(s(z3))))))
MAX(N(L(z0), N(L(z1), N(L(s(s(y1))), L(s(s(y2))))))) → c1(MAX(N(L(z1), N(L(s(s(y1))), L(s(s(y2)))))))
MAX(N(L(s(s(s(y0)))), L(s(s(s(y1)))))) → c2(MAX(N(L(s(s(y0))), L(s(s(y1))))))
MAX(N(L(s(s(s(y0)))), N(L(s(0)), L(s(s(s(y1))))))) → c(MAX(N(L(s(s(s(y0)))), L(s(s(s(y1)))))))
S tuples:

MAX(N(L(s(s(s(y0)))), L(s(s(s(y1)))))) → c2(MAX(N(L(s(s(y0))), L(s(s(y1))))))
K tuples:

MAX(N(L(z0), N(z1, z2))) → c3(MAX(N(L(z0), L(max(N(z1, z2))))), MAX(N(z1, z2)))
Defined Rule Symbols:

max

Defined Pair Symbols:

MAX

Compound Symbols:

c3, c1, c, c3, c2

(37) CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID) transformation)

Use forward instantiation to replace MAX(N(L(s(s(y0))), N(L(0), L(s(s(y1)))))) → c3(MAX(N(L(s(s(y0))), L(s(s(y1)))))) by

MAX(N(L(s(s(s(y0)))), N(L(0), L(s(s(s(y1))))))) → c3(MAX(N(L(s(s(s(y0)))), L(s(s(s(y1)))))))

(38) Obligation:

Complexity Dependency Tuples Problem
Rules:

max(N(L(0), L(z0))) → z0
max(N(L(s(z0)), L(s(z1)))) → s(max(N(L(z0), L(z1))))
max(N(L(z0), N(z1, z2))) → max(N(L(z0), L(max(N(z1, z2)))))
Tuples:

MAX(N(L(x0), N(L(0), N(x2, x3)))) → c3(MAX(N(L(x0), L(max(N(x2, x3))))), MAX(N(L(0), N(x2, x3))))
MAX(N(L(x0), N(L(x1), N(L(z0), N(z1, z2))))) → c3(MAX(N(L(x0), L(max(N(L(x1), L(max(N(L(z0), L(max(N(z1, z2))))))))))), MAX(N(L(x1), N(L(z0), N(z1, z2)))))
MAX(N(L(x0), N(L(x1), N(L(0), L(z0))))) → c1(MAX(N(L(x0), L(max(N(L(x1), L(z0)))))))
MAX(N(L(x0), N(L(x1), N(L(s(z0)), L(s(z1)))))) → c1(MAX(N(L(x0), L(max(N(L(x1), L(s(max(N(L(z0), L(z1)))))))))))
MAX(N(L(x0), N(L(s(s(z0))), L(s(s(z1)))))) → c(MAX(N(L(x0), L(s(s(max(N(L(z0), L(z1)))))))))
MAX(N(L(z0), N(L(s(s(y0))), L(s(s(y1)))))) → c(MAX(N(L(s(s(y0))), L(s(s(y1))))))
MAX(N(L(z0), N(L(s(s(y0))), N(L(0), L(s(s(y1))))))) → c1(MAX(N(L(s(s(y0))), N(L(0), L(s(s(y1)))))))
MAX(N(L(z0), N(L(z1), N(L(s(0)), L(s(z3)))))) → c1(MAX(N(L(z1), N(L(s(0)), L(s(z3))))))
MAX(N(L(z0), N(L(z1), N(L(s(s(y1))), L(s(s(y2))))))) → c1(MAX(N(L(z1), N(L(s(s(y1))), L(s(s(y2)))))))
MAX(N(L(s(s(s(y0)))), L(s(s(s(y1)))))) → c2(MAX(N(L(s(s(y0))), L(s(s(y1))))))
MAX(N(L(s(s(s(y0)))), N(L(s(0)), L(s(s(s(y1))))))) → c(MAX(N(L(s(s(s(y0)))), L(s(s(s(y1)))))))
MAX(N(L(s(s(s(y0)))), N(L(0), L(s(s(s(y1))))))) → c3(MAX(N(L(s(s(s(y0)))), L(s(s(s(y1)))))))
S tuples:

MAX(N(L(s(s(s(y0)))), L(s(s(s(y1)))))) → c2(MAX(N(L(s(s(y0))), L(s(s(y1))))))
K tuples:

MAX(N(L(z0), N(z1, z2))) → c3(MAX(N(L(z0), L(max(N(z1, z2))))), MAX(N(z1, z2)))
Defined Rule Symbols:

max

Defined Pair Symbols:

MAX

Compound Symbols:

c3, c1, c, c2, c3

(39) CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID) transformation)

Use forward instantiation to replace MAX(N(L(z0), N(L(s(s(y0))), L(s(s(y1)))))) → c(MAX(N(L(s(s(y0))), L(s(s(y1)))))) by

MAX(N(L(z0), N(L(s(s(s(y0)))), L(s(s(s(y1))))))) → c(MAX(N(L(s(s(s(y0)))), L(s(s(s(y1)))))))

(40) Obligation:

Complexity Dependency Tuples Problem
Rules:

max(N(L(0), L(z0))) → z0
max(N(L(s(z0)), L(s(z1)))) → s(max(N(L(z0), L(z1))))
max(N(L(z0), N(z1, z2))) → max(N(L(z0), L(max(N(z1, z2)))))
Tuples:

MAX(N(L(x0), N(L(0), N(x2, x3)))) → c3(MAX(N(L(x0), L(max(N(x2, x3))))), MAX(N(L(0), N(x2, x3))))
MAX(N(L(x0), N(L(x1), N(L(z0), N(z1, z2))))) → c3(MAX(N(L(x0), L(max(N(L(x1), L(max(N(L(z0), L(max(N(z1, z2))))))))))), MAX(N(L(x1), N(L(z0), N(z1, z2)))))
MAX(N(L(x0), N(L(x1), N(L(0), L(z0))))) → c1(MAX(N(L(x0), L(max(N(L(x1), L(z0)))))))
MAX(N(L(x0), N(L(x1), N(L(s(z0)), L(s(z1)))))) → c1(MAX(N(L(x0), L(max(N(L(x1), L(s(max(N(L(z0), L(z1)))))))))))
MAX(N(L(x0), N(L(s(s(z0))), L(s(s(z1)))))) → c(MAX(N(L(x0), L(s(s(max(N(L(z0), L(z1)))))))))
MAX(N(L(z0), N(L(s(s(y0))), N(L(0), L(s(s(y1))))))) → c1(MAX(N(L(s(s(y0))), N(L(0), L(s(s(y1)))))))
MAX(N(L(z0), N(L(z1), N(L(s(0)), L(s(z3)))))) → c1(MAX(N(L(z1), N(L(s(0)), L(s(z3))))))
MAX(N(L(z0), N(L(z1), N(L(s(s(y1))), L(s(s(y2))))))) → c1(MAX(N(L(z1), N(L(s(s(y1))), L(s(s(y2)))))))
MAX(N(L(s(s(s(y0)))), L(s(s(s(y1)))))) → c2(MAX(N(L(s(s(y0))), L(s(s(y1))))))
MAX(N(L(s(s(s(y0)))), N(L(s(0)), L(s(s(s(y1))))))) → c(MAX(N(L(s(s(s(y0)))), L(s(s(s(y1)))))))
MAX(N(L(s(s(s(y0)))), N(L(0), L(s(s(s(y1))))))) → c3(MAX(N(L(s(s(s(y0)))), L(s(s(s(y1)))))))
MAX(N(L(z0), N(L(s(s(s(y0)))), L(s(s(s(y1))))))) → c(MAX(N(L(s(s(s(y0)))), L(s(s(s(y1)))))))
S tuples:

MAX(N(L(s(s(s(y0)))), L(s(s(s(y1)))))) → c2(MAX(N(L(s(s(y0))), L(s(s(y1))))))
K tuples:

MAX(N(L(z0), N(z1, z2))) → c3(MAX(N(L(z0), L(max(N(z1, z2))))), MAX(N(z1, z2)))
Defined Rule Symbols:

max

Defined Pair Symbols:

MAX

Compound Symbols:

c3, c1, c, c2, c3

(41) CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID) transformation)

Use forward instantiation to replace MAX(N(L(z0), N(L(s(s(y0))), N(L(0), L(s(s(y1))))))) → c1(MAX(N(L(s(s(y0))), N(L(0), L(s(s(y1))))))) by

MAX(N(L(z0), N(L(s(s(s(y0)))), N(L(0), L(s(s(s(y1)))))))) → c1(MAX(N(L(s(s(s(y0)))), N(L(0), L(s(s(s(y1))))))))

(42) Obligation:

Complexity Dependency Tuples Problem
Rules:

max(N(L(0), L(z0))) → z0
max(N(L(s(z0)), L(s(z1)))) → s(max(N(L(z0), L(z1))))
max(N(L(z0), N(z1, z2))) → max(N(L(z0), L(max(N(z1, z2)))))
Tuples:

MAX(N(L(x0), N(L(0), N(x2, x3)))) → c3(MAX(N(L(x0), L(max(N(x2, x3))))), MAX(N(L(0), N(x2, x3))))
MAX(N(L(x0), N(L(x1), N(L(z0), N(z1, z2))))) → c3(MAX(N(L(x0), L(max(N(L(x1), L(max(N(L(z0), L(max(N(z1, z2))))))))))), MAX(N(L(x1), N(L(z0), N(z1, z2)))))
MAX(N(L(x0), N(L(x1), N(L(0), L(z0))))) → c1(MAX(N(L(x0), L(max(N(L(x1), L(z0)))))))
MAX(N(L(x0), N(L(x1), N(L(s(z0)), L(s(z1)))))) → c1(MAX(N(L(x0), L(max(N(L(x1), L(s(max(N(L(z0), L(z1)))))))))))
MAX(N(L(x0), N(L(s(s(z0))), L(s(s(z1)))))) → c(MAX(N(L(x0), L(s(s(max(N(L(z0), L(z1)))))))))
MAX(N(L(z0), N(L(z1), N(L(s(0)), L(s(z3)))))) → c1(MAX(N(L(z1), N(L(s(0)), L(s(z3))))))
MAX(N(L(z0), N(L(z1), N(L(s(s(y1))), L(s(s(y2))))))) → c1(MAX(N(L(z1), N(L(s(s(y1))), L(s(s(y2)))))))
MAX(N(L(s(s(s(y0)))), L(s(s(s(y1)))))) → c2(MAX(N(L(s(s(y0))), L(s(s(y1))))))
MAX(N(L(s(s(s(y0)))), N(L(s(0)), L(s(s(s(y1))))))) → c(MAX(N(L(s(s(s(y0)))), L(s(s(s(y1)))))))
MAX(N(L(s(s(s(y0)))), N(L(0), L(s(s(s(y1))))))) → c3(MAX(N(L(s(s(s(y0)))), L(s(s(s(y1)))))))
MAX(N(L(z0), N(L(s(s(s(y0)))), L(s(s(s(y1))))))) → c(MAX(N(L(s(s(s(y0)))), L(s(s(s(y1)))))))
MAX(N(L(z0), N(L(s(s(s(y0)))), N(L(0), L(s(s(s(y1)))))))) → c1(MAX(N(L(s(s(s(y0)))), N(L(0), L(s(s(s(y1))))))))
S tuples:

MAX(N(L(s(s(s(y0)))), L(s(s(s(y1)))))) → c2(MAX(N(L(s(s(y0))), L(s(s(y1))))))
K tuples:

MAX(N(L(z0), N(z1, z2))) → c3(MAX(N(L(z0), L(max(N(z1, z2))))), MAX(N(z1, z2)))
Defined Rule Symbols:

max

Defined Pair Symbols:

MAX

Compound Symbols:

c3, c1, c, c2, c3

(43) CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID) transformation)

Use forward instantiation to replace MAX(N(L(z0), N(L(z1), N(L(s(0)), L(s(z3)))))) → c1(MAX(N(L(z1), N(L(s(0)), L(s(z3)))))) by

MAX(N(L(z0), N(L(s(s(s(y0)))), N(L(s(0)), L(s(s(s(y1)))))))) → c1(MAX(N(L(s(s(s(y0)))), N(L(s(0)), L(s(s(s(y1))))))))

(44) Obligation:

Complexity Dependency Tuples Problem
Rules:

max(N(L(0), L(z0))) → z0
max(N(L(s(z0)), L(s(z1)))) → s(max(N(L(z0), L(z1))))
max(N(L(z0), N(z1, z2))) → max(N(L(z0), L(max(N(z1, z2)))))
Tuples:

MAX(N(L(x0), N(L(0), N(x2, x3)))) → c3(MAX(N(L(x0), L(max(N(x2, x3))))), MAX(N(L(0), N(x2, x3))))
MAX(N(L(x0), N(L(x1), N(L(z0), N(z1, z2))))) → c3(MAX(N(L(x0), L(max(N(L(x1), L(max(N(L(z0), L(max(N(z1, z2))))))))))), MAX(N(L(x1), N(L(z0), N(z1, z2)))))
MAX(N(L(x0), N(L(x1), N(L(0), L(z0))))) → c1(MAX(N(L(x0), L(max(N(L(x1), L(z0)))))))
MAX(N(L(x0), N(L(x1), N(L(s(z0)), L(s(z1)))))) → c1(MAX(N(L(x0), L(max(N(L(x1), L(s(max(N(L(z0), L(z1)))))))))))
MAX(N(L(x0), N(L(s(s(z0))), L(s(s(z1)))))) → c(MAX(N(L(x0), L(s(s(max(N(L(z0), L(z1)))))))))
MAX(N(L(z0), N(L(z1), N(L(s(s(y1))), L(s(s(y2))))))) → c1(MAX(N(L(z1), N(L(s(s(y1))), L(s(s(y2)))))))
MAX(N(L(s(s(s(y0)))), L(s(s(s(y1)))))) → c2(MAX(N(L(s(s(y0))), L(s(s(y1))))))
MAX(N(L(s(s(s(y0)))), N(L(s(0)), L(s(s(s(y1))))))) → c(MAX(N(L(s(s(s(y0)))), L(s(s(s(y1)))))))
MAX(N(L(s(s(s(y0)))), N(L(0), L(s(s(s(y1))))))) → c3(MAX(N(L(s(s(s(y0)))), L(s(s(s(y1)))))))
MAX(N(L(z0), N(L(s(s(s(y0)))), L(s(s(s(y1))))))) → c(MAX(N(L(s(s(s(y0)))), L(s(s(s(y1)))))))
MAX(N(L(z0), N(L(s(s(s(y0)))), N(L(0), L(s(s(s(y1)))))))) → c1(MAX(N(L(s(s(s(y0)))), N(L(0), L(s(s(s(y1))))))))
MAX(N(L(z0), N(L(s(s(s(y0)))), N(L(s(0)), L(s(s(s(y1)))))))) → c1(MAX(N(L(s(s(s(y0)))), N(L(s(0)), L(s(s(s(y1))))))))
S tuples:

MAX(N(L(s(s(s(y0)))), L(s(s(s(y1)))))) → c2(MAX(N(L(s(s(y0))), L(s(s(y1))))))
K tuples:

MAX(N(L(z0), N(z1, z2))) → c3(MAX(N(L(z0), L(max(N(z1, z2))))), MAX(N(z1, z2)))
Defined Rule Symbols:

max

Defined Pair Symbols:

MAX

Compound Symbols:

c3, c1, c, c2, c3